g:IMonoid, i, j:.
(i < j)
 (E:({i..j}|g|). (*,e) i  k < j. E(k) = ((*,e) i  k < j - 1. E(k) * E(j - 1))  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid, (op,id) lb  i < ub. E(i)
Definitions	, t  T, P  Q, x:A. B(x), True, T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , Y, (op,id) lb  i < ub. E(i), False, A, A  B, i  j < k, x. t(x), x(s), x f y, {i..j}, IMonoid, Unit, ,
Lemmas	imon wf, grp car wf, int seg wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, bnot wf, le wf, le int wf, assert of lt int, eqtt to assert, assert wf, iff transitivity, bool wf, lt int wf, grp id wf, itop wf, grp op wf